The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

m2(S(0), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0, b, res, True) → False
m3(S(0), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0, b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0
help1(S(0)) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0)), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0, y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0) → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0, tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0, False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
m4(S(x'), S(x), res, t) →⁺ m5(S(x'), S(x), m4(x', x, False, False), t)
gives rise to a decreasing loop by considering the right hand sides subterm at position [2].
The pumping substitution is [x' / S(x'), x / S(x)].
The result substitution is [res / False, t / False].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
l15, gcd, l13, m4, monus, m2, l8, l10, l5, l7, l2, l3, l11, l14, l12, l4, <

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m2
monus = m2
monus < l14
monus < l12
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
< < l10
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(8) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
<, l15, gcd, l13, m4, monus, m2, l8, l10, l5, l7, l2, l3, l11, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m2
monus = m2
monus < l14
monus < l12
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
< < l10
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Induction Base:
<(gen_0':S34_17(0), gen_0':S34_17(+(1, 0))) →_R^Ω(0)
True

Induction Step:
<(gen_0':S34_17(+(n36_17, 1)), gen_0':S34_17(+(1, +(n36_17, 1)))) →_R^Ω(0)
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) →_IH
True

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n⁰).

(10) Complex Obligation (BEST)

(11) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
monus, l15, gcd, l13, m4, m2, l8, l10, l5, l7, l2, l3, l11, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m2
monus = m2
monus < l14
monus < l12
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol monus.

(13) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
m2, l15, gcd, l13, m4, l8, l10, l5, l7, l2, l3, l11, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m2
monus = m2
monus < l14
monus < l12
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(14) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol m2.

(15) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
m4, l15, gcd, l13, l8, l10, l5, l7, l2, l3, l11, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m2
monus = m2
monus < l14
monus < l12
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(16) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol m4.

(17) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
gcd, l15, l13, l8, l10, l5, l7, l2, l3, l11, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(18) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol gcd.

(19) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l2, l15, l13, l8, l10, l5, l7, l3, l11, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(20) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l2.

(21) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l3, l15, l13, l8, l10, l5, l7, l11, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l3.

(23) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l4, l15, l13, l8, l10, l5, l7, l11, l14, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(24) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l4.

(25) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l5, l15, l13, l8, l10, l7, l11, l14, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(26) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l5.

(27) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l7, l15, l13, l8, l10, l11, l14, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(28) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l7.

(29) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l8, l15, l13, l10, l11, l14, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(30) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l8.

(31) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l10, l15, l13, l11, l14, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(32) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l10.

(33) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l11, l15, l13, l14, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(34) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l11.

(35) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l14, l15, l13, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(36) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l14.

(37) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l15, l13, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(38) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l15.

(39) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l12, l13

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(40) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l12.

(41) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

The following defined symbols remain to be analysed:
l13

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4

(42) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l13.

(43) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

No more defined symbols left to analyse.

(44) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

(45) BOUNDS(1, INF)

(46) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S

Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))

No more defined symbols left to analyse.

(47) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)

(48) BOUNDS(1, INF)